the_es:ES, e:E. ((isrcv(e)))  (act(e)  Id) 

latex

Definitions	t  T, x:A. B(x), kind(e), isrcv(k), x:AB(x), P  Q, P  Q, x:A  B(x), P & Q, P  Q, b, A, act(k), es_info(es), kind(e), act(e), isrcv(e), E, ES, Id
Lemmas	event system wf, actof wf, not wf, assert wf, islocal-not-isrcv, assert of bnot, isrcv wf, kind wf